<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">

<html>
<head>

<title>
PRISM Manual | Main / Contents 
</title>

<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="keywords" content="prism, probabilistic, symbolic, model, checker, verification, birmingham, oxford, parker, norman, kwiatkowska">

<link rel="icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">
<link rel="shortcut icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">

<!--HTMLHeader--><style type='text/css'><!--
  ul, ol, pre, dl, p { margin-top:0px; margin-bottom:0px; }
  code.escaped { white-space: nowrap; }
  .vspace { margin-top:1.33em; }
  .indent { margin-left:40px; }
  .outdent { margin-left:40px; text-indent:-40px; }
  a.createlinktext { text-decoration:none; border-bottom:1px dotted gray; }
  a.createlink { text-decoration:none; position:relative; top:-0.5em;
    font-weight:bold; font-size:smaller; border-bottom:none; }
  img { border:0px; }
  .editconflict { color:green; 
  font-style:italic; margin-top:1.33em; margin-bottom:1.33em; }

  table.markup { border:2px dotted #ccf; width:90%; }
  td.markup1, td.markup2 { padding-left:10px; padding-right:10px; }
  table.vert td.markup1 { border-bottom:1px solid #ccf; }
  table.horiz td.markup1 { width:23em; border-right:1px solid #ccf; }
  table.markup caption { text-align:left; }
  div.faq p, div.faq pre { margin-left:2em; }
  div.faq p.question { margin:1em 0 0.75em 0; font-weight:bold; }
  div.faqtoc div.faq * { display:none; }
  div.faqtoc div.faq p.question 
    { display:block; font-weight:normal; margin:0.5em 0 0.5em 20px; line-height:normal; }
  div.faqtoc div.faq p.question * { display:inline; }
   
    .frame 
      { border:1px solid #cccccc; padding:4px; background-color:#f9f9f9; }
    .lfloat { float:left; margin-right:0.5em; }
    .rfloat { float:right; margin-left:0.5em; }
a.varlink { text-decoration:none; }

--></style>  <meta name='robots' content='index,follow' />


<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/base.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prism.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prismmanual.css">

</head>

<body text="#000000" bgcolor="#ffffff">

<div id="layout-maincontainer">
<div id="layout-main">

<div id="prism-mainbox">

<!-- ============================================================================= -->

<!--PageHeaderFmt-->
<!--/PageHeaderFmt-->

<!--PageTitleFmt-->
  <div id="prism-man-title">
    <p><a class='wikilink' href='Welcome.html'>Main</a> /
</p><h1>Contents</h1>

  </div>
<!--PageText-->
<div id='wikitext'>
<h1><a class='wikilink' href='Introduction.html'>Introduction</a></h1>
<div class='vspace'></div><h1><a class='wikilink' href='../InstallingPRISM/Instructions.html'>Installing PRISM</a></h1>
<ul><li><a class='wikilink' href='../InstallingPRISM/Instructions.html'>Instructions</a>
</li><li><a class='wikilink' href='../InstallingPRISM/CommonProblemsAndQuestions.html'>Common Problems And Questions</a>
</li></ul><div class='vspace'></div><h1><a class='wikilink' href='../ThePRISMLanguage/Introduction.html'>The PRISM Language</a></h1>
<ul><li><a class='wikilink' href='../ThePRISMLanguage/Introduction.html'>Introduction</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/Example1.html'>Example 1</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/ModelType.html'>Model Type</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/ModulesAndVariables.html'>Modules And Variables</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/Commands.html'>Commands</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/ParallelComposition.html'>Parallel Composition</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/LocalNondeterminism.html'>Local Nondeterminism</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/CTMCs.html'>CTMCs</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/Example2.html'>Example 2</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/Constants.html'>Constants</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/Expressions.html'>Expressions</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/Synchronisation.html'>Synchronisation</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/ModuleRenaming.html'>Module Renaming</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/MultipleInitialStates.html'>Multiple Initial States</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/GlobalVariables.html'>Global Variables</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/FormulasAndLabels.html'>Formulas And Labels</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/PTAs.html'>PTAs</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/CostsAndRewards.html'>Costs And Rewards</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/ProcessAlgebraOperators.html'>Process Algebra Operators</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/PRISMModelFiles.html'>PRISM Model Files</a>
</li></ul><div class='vspace'></div><h1><a class='wikilink' href='../PropertySpecification/Introduction.html'>Property Specification</a></h1>
<ul><li><a class='wikilink' href='../PropertySpecification/Introduction.html'>Introduction</a>
</li><li><a class='wikilink' href='../PropertySpecification/IdentifyingASetOfStates.html'>Identifying A Set Of States</a>
</li><li><a class='wikilink' href='../PropertySpecification/ThePOperator.html'>The P Operator</a>
</li><li><a class='wikilink' href='../PropertySpecification/TheSOperator.html'>The S Operator</a>
</li><li><a class='wikilink' href='../PropertySpecification/Reward-basedProperties.html'>Reward-based Properties</a>
</li><li><a class='wikilink' href='../PropertySpecification/SyntaxAndSemantics.html'>Syntax And Semantics</a>
</li><li><a class='wikilink' href='../PropertySpecification/Filters.html'>Filters</a>
</li><li><a class='wikilink' href='../PropertySpecification/PTAProperties.html'>PTA Properties</a>
</li><li><a class='wikilink' href='../PropertySpecification/PropertiesFiles.html'>Properties Files</a>
</li></ul><div class='vspace'></div><h1><a class='wikilink' href='../RunningPRISM/StartingPRISM.html'>Running PRISM</a></h1>
<ul><li><a class='wikilink' href='../RunningPRISM/StartingPRISM.html'>Starting PRISM</a>
</li><li><a class='wikilink' href='../RunningPRISM/LoadingAndBuildingAModel.html'>Loading And Building a Model</a>
</li><li><a class='wikilink' href='../RunningPRISM/DebuggingModelsWithTheSimulator.html'>Debugging Models With The Simulator</a>
</li><li><a class='wikilink' href='../RunningPRISM/ExportingTheModel.html'>Exporting The Model</a>
</li><li><a class='wikilink' href='../RunningPRISM/ModelChecking.html'>Model Checking</a>
</li><li><a class='wikilink' href='../RunningPRISM/ApproximateModelChecking.html'>Approximate Model Checking</a>
</li><li><a class='wikilink' href='../RunningPRISM/ComputingSteady-stateAndTransientProbabilities.html'>Computing Steady-state And Transient Probabilities</a>
</li><li><a class='wikilink' href='../RunningPRISM/Experiments.html'>Experiments</a>
</li><li><a class='wikilink' href='../RunningPRISM/Adversaries.html'>Adversaries</a>
</li><li><a class='wikilink' href='../RunningPRISM/SupportForPEPAModels.html'>Support For PEPA Models</a>
</li><li><a class='wikilink' href='../RunningPRISM/SupportForSBML.html'>Support For SBML</a>
</li><li><a class='wikilink' href='../RunningPRISM/ExplicitModelImport.html'>Explicit Model Import</a>
</li></ul><div class='vspace'></div><h1><a class='wikilink' href='../ConfiguringPRISM/Introduction.html'>Configuring PRISM</a></h1>
<ul><li><a class='wikilink' href='../ConfiguringPRISM/Introduction.html'>Introduction</a>
</li><li><a class='wikilink' href='../ConfiguringPRISM/ComputationEngines.html'>Computation Engines</a>
</li><li><a class='wikilink' href='../ConfiguringPRISM/IterativeNumericalMethods.html'>Iterative Numerical Methods</a>
</li><li><a class='wikilink' href='../ConfiguringPRISM/OtherOptions.html'>Other Options</a>
</li></ul><div class='vspace'></div><h1><a class='wikilink' href='References.html'>References</a></h1>
</div>


<!--PageFooterFmt-->
  <div id='prism-man-footer'>
  </div>
<!--/PageFooterFmt-->


<!-- ============================================================================= -->

</div> <!-- id="prism-mainbox" -->

</div> <!-- id="layout-main" -->
</div> <!-- id="layout-maincontainer" -->

<div id="layout-leftcol">
<div id="prism-navbar2">

<h3><a class='wikilink' href='Welcome.html'>PRISM Manual</a></h3>
<ul><li><a class='selflink' href='Contents.html'>Contents</a>
</li><li><a class='wikilink' href='Introduction.html'>Introduction</a>
</li><li><a class='wikilink' href='../InstallingPRISM/Instructions.html'>Installing PRISM</a>
</li><li><a class='wikilink' href='../ThePRISMLanguage/Introduction.html'>The PRISM Language</a>
</li><li><a class='wikilink' href='../PropertySpecification/Introduction.html'>Property Specification</a>
</li><li><a class='wikilink' href='../RunningPRISM/StartingPRISM.html'>Running PRISM</a>
</li><li><a class='wikilink' href='../ConfiguringPRISM/Introduction.html'>Configuring PRISM</a>
</li><li><a class='wikilink' href='References.html'>References</a>
</li><li><a class='wikilink' href='../FrequentlyAskedQuestions/Main.html'>FAQ</a>
</li></ul><p>[ <a class='wikilink' href='AllOnOnePage.html'>View all</a> ]
</p>


</div>  <!-- id="prism-navbar2" -->
</div> <!-- id="layout-leftcol" -->

</body>
</html>
